Search results for "counting quantifiers"
showing 3 items of 3 documents
Adding Path-Functional Dependencies to the Guarded Two-Variable Fragment with Counting
2017
The satisfiability and finite satisfiability problems for the two-variable guarded fragment of first-order logic with counting quantifiers, a database, and path-functional dependencies are both ExpTime-complete.
Fluted Logic with Counting
2021
The fluted fragment is a fragment of first-order logic in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. It is known that the fluted fragment possesses the finite model property. In this paper, we extend the fluted fragment by the addition of counting quantifiers. We show that the resulting logic retains the finite model property, and that the satisfiability problem for its (m+1)-variable sub-fragment is in m-NExpTime for all positive m. We also consider the satisfiability and finite satisfiability problems for the extension of any of these fragments in which the fluting requirement applies only to sub-form…
Two-variable First-Order Logic with Counting in Forests
2018
We consider an extension of two-variable, first-order logic with counting quantifiers and arbitrarily many unary and binary predicates, in which one distinguished predicate is interpreted as the mother-daughter relation in an unranked forest. We show that both the finite satisfiability and the general satisfiability problems for the extended logic are decidable in NExpTime. We also show that the decision procedure for finite satisfiability can be extended to the logic where two distinguished predicates are interpreted as the mother-daughter relations in two independent forests.